Inference at * 1 1 
Iof proof for Lemma decidable-filter:



1. T : Type
2. T List
3. P : {x:T| (x  [])} 
4. x[]. Dec(P(x))
  []  [] 

latex

 by ((BLemma `nil_sublist`) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	x:A. B(x), P  Q, P & Q, x:A  B(x), P  Q, P  Q, x:AB(x), L1  L2, True, t  T
Lemmas	nil sublist